\begin{tabbing}
$\forall$\=$A$, $C$:Type, $B$:($A$$\rightarrow$Type), ${\it eqa}$:EqDecider($A$), ${\it eqc}$, ${\it eqc'}$:EqDecider($C$), $r$:($A$$\rightarrow$$C$),\+
\\[0ex]$f$:$a$:$A$ fp$\rightarrow$ $B$($a$), $a$:$A$. Inj($A$;$C$;$r$) $\Rightarrow$ ($\uparrow$$a$ $\in$ dom($f$)) $\Rightarrow$ (rename($r$;$f$)($r$($a$)) = $f$($a$) $\in$ $B$($a$))
\-
\end{tabbing}